COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	second application: the case of lists of numbers
C00003 00003	Disjointness
C00006 00004	lemma into_mult
C00007 00005	the main result for perm
C00009 ENDMK
C⊗;
;second application: the case of lists of numbers
(wipe-out)
(get-proofs pigeon prf ekl sys)
(proof lpig)

(axiom |∀n m.(un((λxv.mkset xv),n))(m)⊃m<n|)
(label dn1)

;Lemma disjoint_number:

(axiom |∀n.disjoint(λxv.mkset xv,n)|)
(label disjoint_number)

(axiom |∀u.into(u)∧(∀k.k<length u⊃1=mult(u,mkset(k)))⊃
                   (∀i.i<length u⊃1=mult(u,mkset(nth(u,i))))|)
(label into_mult)

;Theorem

;∀U.PERM(U)⊃INJ(U)
;perm injectvity
(save-proofs lpig)
;Disjointness
(proof disjoint_number)

;lemma dn1

1.  (ue (a |λn.∀m.(un((λxv.mkset(xv)),n))(m)⊃m<n|)
        proof_by_induction 
        (part 1(open mkset un emptyset union))
        (use normal mode: always)
        (use successor1 transitivity_of_order))
    ;∀N M.(UN(λXV.MKSET(XV),N))(M)⊃M<N

;LEMMA
;∀N M.(UN(λXV.(λX.X=XV),N))(M)⊃M<N
;if a number M belongs to the set ∪({I})I<N, then I is less than N....

;lemma disjoint number

2.  (ue ((n.n)(m.n)) dn1  irreflexivity_of_order)
    ;¬(UN(λXV.MKSET(XV),N))(N)

3.  (trw |(un(λyv.mkset(yv),n))(xv)∧(mkset(n))(xv)| * (part 2(open mkset)))
    ;¬((UN(λYV.MKSET(YV),N))(XV)∧(MKSET(N))(XV))

4.  (ue (a |λn.disjoint(λxv.mkset(xv),n)|) proof_by_induction 
        (open disjoint disj_pair emptyp intersection) 
        (use * mode: exact))
    ;∀N.DISJOINT(λXV.MKSET(XV),N)

;LEMMA
;∀N.DISJOINT(λXV.MKSET(XV),N)
;...Therefore ∪({I})I<N and {N} have empty intersection and so, by induction on N
;∪({I})I<N is DISJOINT.

;;;;;;;;;;
;Exercise: Prove the converse of DN1:
;UN(λXV.(λX.X=XV),N)=(λXV.XV<N)

;(rw less_succ_lesseq (open lesseq))
;∀N M.M<N'≡M=N∨M<N

;(ue (a |λn.∀m.m<n⊃(un(λxv.(λx.x=xv),n))(m)|) proof_by_induction  (open un union)
;       (use * mode: exact) (use normal mode: always))
;∀N M.M<N⊃(UN(λXV.(λX.X=XV),N))(M)
;(label dn3)

;(derive |∀n m.(un(λxv.(λx.x=xv),n))(m)≡(λxv.xv<n)(m)| (dn1 dn3))

;(ue ((a.|un(λxv.λx.x=xv,n)|)(b.|λxv.xv<n|)) set_extensionality * (open epsilon))
;UN(λXV.(λX.X=XV),N)=(λXV.XV<N)

;lemma into_mult

    (proof into_mult)

1.  (assume |into(u)|)
    (label im1)

2.  (assume |∀k.k<length u⊃1=mult(u,mkset k)|)
    (label im2)

3.  (assume |i<length u|)
    (label im3)

4.  (rw im1 (open into))
    ;∀N.N<LENGTH U⊃NATNUM(NTH(U,N))∧NTH(U,N)<LENGTH U
    ;deps: (IM1)

5.  (ue (k |nth(u,i)|) im2 (use im3 * mode: exact))
    ;1=MULT(U,MKSET(NTH(U,I)))
    ;deps: (IM1 IM2 IM3)

6.  (ci im3)
    ;I<LENGTH U⊃1=MULT(U,MKSET(NTH(U,I)))
    ;deps: (IM1 IM2)

7.  (ci (im1 im2))
    ;INTO(U)∧(∀K.K<LENGTH U⊃1=MULT(U,MKSET(K)))⊃
    ;(I<LENGTH U⊃1=MULT(U,MKSET(NTH(U,I))))

;the main result for perm
;a straightforward application of pigeon hole to onto lists

    (proof perm_inj)
    ;∀U.PERM(U)⊃INJ(U)

1.  (assume |perm u|)
    (label perm_inj1)

2.  (rw * (open perm onto))
    ;INTO(U)∧(∀N.N<LENGTH U⊃MEMBER(N,U))
    (label perm_inj2)

;labels: MEMBER_MULT 
;(AXIOM |∀U Y A.MEMBER(Y,U)∧A(Y)⊃1≤MULT(U,A)|)

3.  (ue ((u.u)(y.n)(a.|mkset n|)) member_mult 
      (part 1(open mkset)))
    ;MEMBER(N,U)⊃1≤MULT(U,MKSET(N))

4.  (derive |∀n.n<length u⊃1≤mult(u,mkset n)| (perm_inj2 *))
    (label onto_mult)(label perm_inj3) 
    ;deps: (PERM_INJ1)

5.  (ue ((setseq.|λxv.mkset(xv)|)(u.u)) pigeonlist disjoint_number perm_inj3)
    ;∀K.K<LENGTH U⊃1=MULT(U,MKSET(K))
    (label perm_inj4)
    ;deps: (PERM_INJ1)

;labels: INTO_MULT 
;∀U.INTO(U)∧(∀K.K<LENGTH U⊃1=MULT(U,MKSET(K)))⊃
;           (∀I.I<LENGTH U⊃1=MULT(U,MKSET(NTH(U,I))))
      
6.  (derive |∀i.i<length u⊃1=mult(u,mkset(nth(u,i)))| (into_mult perm_inj2 *))
    ;deps: (PERM_INJ1)

;labels: MULT_INJ 
;∀V.(∀K.K<LENGTH V⊃MULT(V,MKSET(NTH(V,K)))=1)⊃INJ(V)

7.  (ue (v u) mult_inj *)
    ;INJ(U)
    ;deps: (PERM_INJ1)

8.  (ci perm_inj1)
    ;PERM(U)⊃INJ(U)
    (label perm_injectvity)